1. Field of the Invention
The present invention generally relates to code validation or verification techniques and, in particular, to a code verification system and method for checking compiled code for type errors.
2. Related Art
During compiling, computer code is often checked for errors before the computer code is allowed to execute. Such testing helps to ensure that data errors do not occur during execution. However, a set of computer code is not always compiled by a trusted source. For example, compiled computer code (e.g., bytecode) that is to be executed by a user's computer may be downloaded from an unknown or distrusted computer that compiled the code. Such a situation frequently occurs when a user utilizes the Internet. In this regard, it is common for on-line users of the Internet to download compiled code from distrusted servers and to execute the downloaded code on the user's computer.
Because the downloaded code may not be compiled by a trusted source, it is possible for that code to contain errors that are detectable via proper error checking typically performed during compilation. These errors may be inadvertent, such as, for example, when inadvertent data transmission errors occur during the downloading process, or the errors may be intentional, such as, for example, when a hacker intentionally introduces errors into the code in an attempt compromise the operation or security of the user's computer. Thus, when compiled computer code is downloaded into a user's computer for execution on the user's computer, it is often desirable to check the code to ensure that the code does not contain certain potential data errors, particularly when the compiled code is downloaded from a distrusted source. Such checking is sometimes referred to as “code verification” or “code validation” and is normally performed before the downloaded code is executed.
Note that cryptographic signing of code may be utilized to identify whether or not downloaded code has been transmitted from a trusted source. In this regard, if downloaded code has been signed by a source that the user's computer recognizes as a trusted source, then performing code verification on the downloaded code may not be necessary. However, if the downloaded code does not include such a signature, then it may be desirable for the user's computer to perform code verification on the code before executing the code.
An important test typically performed by code verification is type checking. In type checking, code is analyzed to ensure that each consuming instruction of the code will at least be provided with inputs (e.g., arguments) of the correct type. In this regard, it is well known that values processed by a computer are typically assigned a type and that certain instructions should only execute based on particular types of inputs. Typical examples of different value types include, but are not limited to, “int,” “floating,” “double,” “String,” etc. As an example, an add instruction may require two “int” inputs for execution. If, during execution, the add instruction is provided an input of a different type (e.g., “double”), an execution error may occur. Thus, in type checking, potential errors caused by instructions being provided wrong types of inputs are detected.
Note that in object-oriented programming languages (e.g., C++ or JAVA), a value type may be a class that is defined within the program. Further, a class may be extended or derived by various subclasses. If an instruction should receive an input of a particular class during execution, then an error should not occur if the instruction is provided an argument of the particular class or of a sub-class of the particular class. However, if it is determined in performing code verification that the instruction, when executed, will be provided with an input of a different class or type, then a potential type error should be detected by the code verification process. Otherwise, the instruction should pass the type checking performed by the code verification process.
In conventional computers, code verification of compiled code is often achieved by performing a symbolic execution (i.e, a simulation) of the compiled code before actually executing the code. Such code verification is generally described in U.S. Pat. Nos. 5,740,441; 5,668,999; and 5,748,964, which are incorporated herein by reference. During symbolic execution, determinations can be made as to which types of values are symbolically pulled from and pushed to the computer's stack for each symbolically executed instruction. An error is detected if it can be determined that an instruction is provided with a wrong type of input during the symbolic execution.